$\forall$$D$, ${\it D'}$:dsys\{i:l\}, $P$:(\{${\it es}$:ES\{i\}$\mid$ d{-}es\{i:l\}($D$; ${\it es}$) \}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]d{-}realizes\{i:l\}($D$; ${\it es}$.$P$(${\it es}$)) $\Rightarrow$ \{d{-}sub\{i:l\}($D$; ${\it D'}$) $\Rightarrow$ d{-}realizes\{i:l\}(${\it D'}$; ${\it es}$.$P$(${\it es}$))\}